\begin{tabbing}
R{-}base{-}ma($R$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $R$ of \+
\\[0ex]Rnone =$>$ 
\\[0ex]Rplus(${\it left}$,${\it right}$)=$>$${\it rec}_{1}$,${\it rec}_{2}$.
\\[0ex]Rinit(${\it loc}$,$T$,$x$,$V$)=$>$ case $V$
\\[0ex]o\=f inl($v$) =$>$ $x$ : $T$ initially $x$ = $\lambda$$t$.$v$\+
\\[0ex]$\mid$ inr($v$) =$>$ $x$ : $T$ initially $x$ = $v$
\-\\[0ex]Rframe(${\it loc}$,$T$,$x$,$L$)=$>$ only members of $L$ affect $x$ :$T$
\\[0ex]Rsframe(${\it lnk}$,${\it tag}$,$L$)=$>$ only $L$ sends on (${\it lnk}$ with ${\it tag}$)
\\[0ex]Reffect(${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$F$)=$>$ case $F$
\\[0ex]o\=f inl($f$) =$>$ \=with declarations \+\+
\\[0ex]ds:${\it ds}$
\\[0ex]da:${\it knd}$ : $T$
\\[0ex]effect of ${\it knd}$(v) is $x$ := $\lambda$$s$,$v$,$t$. $f$($s$,$v$) s v
\-\\[0ex]$\mid$ inr($f$) =$>$ \=with declarations \+
\\[0ex]ds:${\it ds}$
\\[0ex]da:${\it knd}$ : $T$
\\[0ex]effect of ${\it knd}$(v) is $x$ := $f$ s v
\-\-\\[0ex]Rsends(${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$)=$>$ with declarations 
\\[0ex]ds:${\it ds}$
\\[0ex]da:${\it knd}$ : $T$ $\oplus$ lnk{-}decl($l$;${\it dt}$)
\\[0ex]${\it knd}$(v) sends $g$ s v on link $l$
\\[0ex]R\=pre(${\it loc}$,${\it ds}$,$a$,$p$,$P$)=$>$ (precondition $a$:Outcome($p$) is\+
\\[0ex]$P$:State(${\it ds}$) {-}$>$ Bool)
\-\\[0ex]Rkframe(${\it loc}$,$k$,$L$)=$>$ $k$ affects only members of $L$
\\[0ex]Rksframe(${\it loc}$,$k$,$L$)=$>$ $k$ sends only on links in $L$
\\[0ex]Rrframe(${\it loc}$,$x$,$L$)=$>$ only members of $L$ read $x$
\-
\end{tabbing}